Technologies for inspecting the specifications and configurations of a network are known. As an example of such technologies, for example, NPL 1 mentions a technique known as HSA (Header Space Analysis). In the HSA, a packet header is regarded as a bit series of “L” bits. Each packet is regarded as a certain point in an L-dimension space Π. And it is regarded that a packet is transferred from a certain point to another point in that space Π. Furthermore, a transfer function “ϕ: (Π×P)→Power(Π×E)” which indicates a packet transfer rule is created for each switch apparatus. Here, “X×Y” represents a set of direct products of “X” and “Y”. “Power(X)” represents a power set of “X”.
Here, “P” represents a set of physical switch ports in the network. Hereinafter, a physical switch port is also mentioned simply as port. It is assumed that, in the network, a port is uniquely identified.
“E” is a set of flow entries in the network. A flow entry is constituted by information that represents an input port, a matching pattern, an action, and an output port. Each switch apparatus includes a flow entry. When the header of a packet from the input port matches the matching pattern, the switch apparatus rewrites the header on the basis of the action in case the action is defined, and transfers the packet to the output port. Hereinafter, the pattern of a packet header is also mentioned as packet pattern.
The transfer function ϕ(π, p)={(π′, e)} indicates that when a packet having a packet pattern “π” is input to a certain port “p”, the packet pattern matches a flow entry “e” and the packet header thereof becomes “π”. The input to the transfer function “ϕ” is a pair of the packet pattern of an input packet and the input port of the packet. Because there may be a plurality of flow entries, for one packet, for copying and transferring the packet, the outputs from the transfer function “ϕ” are a set of pairs of the packet pattern of an output packet and a flow entry being matched to the packet.
In HSA, a transfer path of a packet is determined by transitively applying a pair of the transfer function “ϕ” and a connection function σ: P→P that represents a port connection relation between physical switches. And, by transitively applying transfer functions “ϕ” according to the transfer path of the packet, a packet pattern of the packet is determined at a terminating end switch port. HSA traces the path reversely from the determined packet pattern at the terminating end switch port to a starting end switch port, sequentially applying inverse functions ϕe−1: Π→Π of the transfer functions. Therefore, HSA can determine what packet pattern of a header is set to a packet that reaches the terminating end switch port from the starting end switch port includes. In the above, “e” is a flow entry that is applied when the transfer function is applied. That is, in the case where the transfer function is ϕ(π, p)={(π′, e)}, ϕe−1(π′)=π″ indicates that the input packet pattern is narrowed down from “π” to “π″” by re-applying the flow entries in the backward direction.
In the below, a port that is connected to an external network in view of the entire network is referred to as endpoint switch port or endpoint. An input packet that is input to an endpoint is referred to as “incoming packet” and an output packet that is output from an endpoint is referred to as outgoing packet. An endpoint to which an incoming packet is input is referred to as incoming port, and an endpoint from which an outgoing packet is output is referred to as outgoing port. The packet pattern of an incoming packet is referred to as incoming packet pattern, and the packet pattern of an outgoing packet is referred to as outgoing packet pattern.
With regard to any given pair of an incoming port and an outgoing port, by calculating the incoming packet pattern thereof, a network manager can inspect the reaching capability and the isolation property. Here, the reaching capability means that an assumed packet pattern can reach an outgoing port from an incoming port. The isolation property means that an unexpected packet pattern cannot arrive at an outgoing port from an incoming port.